﻿// Spun AJAX Framework
// Copyright (C) 2008 Blake Hegerle
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Formality.FormalSystem;

namespace Formality.Logic.Game
{
    public class Submission
    {
        public enum ResponseType
        {
            Rejected,
            Accepted,
            Proved,
            Finished
        }

        internal Submission(Sentence Sentence, ResponseType Response, Inference? Inference)
        {
            this.Sentence = Sentence;
            this.Response = Response;
            this.Inference = Inference;
        }

        public Inference? Inference { get; private set; }
        public Sentence Sentence { get; private set; }
        public ResponseType Response { get; private set; }

        public override string ToString()
        {
            if (Response == ResponseType.Accepted && Inference.HasValue)
                return string.Format("{0}\t{1}\t{2}", Sentence.Id, Sentence, Inference);
            else
                return string.Format("{0}\t{1}\t{2}", Sentence.Id, Sentence, Response.ToString());
        }
    }

    public class ActiveGame
    {
        public ActiveGame(Engine Engine, Player Player)
        {
            this.Engine = Engine;
            Goal = Engine[Player.ProblemId];

            foreach (var Sub in Player.CurrentProblemSubmissions)
            {
                Proposition Parsed;
                Inference? Inference;

                Follows(Sub, out Parsed, out Inference);

                Submission.ResponseType Resp = Inference.HasValue
                    ? Submission.ResponseType.Accepted
                    : Submission.ResponseType.Rejected;

                submissionList.Add(new Submission(Parsed, Resp, Inference));
            }

            this.Player = Player;
        }

        public Player Player { get; private set; }
        public Sentence Goal
        {
            get { return goal; }
            set
            {
                submissionList = new List<Submission>();
                goal = value;
                Counter = 0;

                if (Player != null)
                    Player.ChangeGoal(value.Id);
            }
        }

        public IEnumerable<Submission> Submissions
        {
            get
            {
                foreach (var S in submissionList)
                    yield return S;
            }
        }
        public IEnumerable<Sentence> Premises
        {
            get { return Engine.GetPremises(goal.Id); }
        }

        public Submission Submit(string Input)
        {
            Proposition Parsed;
            Inference? Inference;

            Follows(Input, out Parsed, out Inference);

            var Resp = UpdateState(Parsed, Inference);
            var Sub = new Submission(Parsed, Resp, Inference);

            if (Resp == Submission.ResponseType.Accepted
                || Resp == Submission.ResponseType.Rejected)
                submissionList.Add(Sub);

            return Sub;
        }

        private void Follows(string Input, out Proposition Parsed, out Inference? Inference)
        {
            if (Input == "prop")
                Input = Goal.ToString();

            if (DidGoto(Input))
            {
                Parsed = null;
                Inference = null;
                return;
            }

            Parsed = Sentence.Parse(Input) as Proposition;

            if (Parsed == null)
                throw new Exception("You must enter a proposition");

            Parsed.DisplayId = Parsed.Id = "(" + ++Counter + ")";

            var Premises = this.Premises.Concat(from S in submissionList
                                            where S.Response == Submission.ResponseType.Accepted
                                            select S.Sentence).ToList();

            Inference = Engine.Follows(Parsed, Enumerable.Reverse(Premises));
        }

        private bool DidGoto(string Input)
        {
            var GotoCommand = "goto ";

            if (Input.StartsWith(GotoCommand))
            {
                Input = Input.Remove(0, GotoCommand.Length);

                Goal = Engine[Input];

                return true;
            }

            return false;
        }

        private Submission.ResponseType UpdateState(Proposition Parsed, Inference? Inference)
        {
            Submission.ResponseType Resp;
            if (Inference.HasValue)
            {
                if (Player != null)
                    Player.AddSubmission(Parsed, Counter);

                if (Parsed.Equals(Goal) == false)
                {
                    Resp = Submission.ResponseType.Accepted;
                }
                else
                {
                    Resp = Submission.ResponseType.Proved;

                    var NextId = Engine.Next(Goal.Id);

                    if (NextId != null)
                    {
                        Goal = Engine[NextId];
                    }
                    else
                    {
                        Resp = Submission.ResponseType.Finished;
                        goal = null;
                    }
                }
            }
            else
            {
                Resp = Submission.ResponseType.Rejected;
            }
            return Resp;
        }

        public override string ToString()
        {
            var Buffer = new StringBuilder();

            Buffer.AppendFormat("Game with {0}\n", Player.Name);

            foreach (var P in Premises)
                Buffer.AppendFormat("\t{0}\t{1}\n", P.DisplayId, P);

            foreach (var Sub in submissionList)
                Buffer.AppendFormat("\t{1}\t{0}\n", Sub.Sentence, Status(Sub));

            Buffer.AppendFormat("Goal: {0}\n", Goal);

            return Buffer.ToString();
        }

        private string Status(Submission Sub)
        {
            switch (Sub.Response)
            {
                case Submission.ResponseType.Finished:
                    return "YOU WON";
                case Submission.ResponseType.Proved:
                    return "QED";
                case Submission.ResponseType.Rejected:
                    return "!";
            }

            return Sub.Sentence.DisplayId;
        }

        private List<Submission> submissionList;
        private Engine Engine;
        private Sentence goal;
        private int Counter;
    }
}
